- (~=~) : (x : a) ->
(y : b) ->
Type
Explicit heterogeneous ("John Major") equality. Use this when Idris
incorrectly chooses homogeneous equality for (=).
- Fixity
- Non-associative, precedence 5
- a
the type of the left side
- b
the type of the right side
- x
the left side
- y
the right side
- void : Void ->
a
The eliminator for the Void type.
- unsafePerformPrimIO : PrimIO a ->
a
- unsafePerformIO : IO' ffi
a ->
a
- trans : (a =
b) ->
(b =
c) ->
a =
c
Transitivity of propositional equality
- sym : (l =
r) ->
r =
l
Symmetry of propositional equality
- run__provider : IO a ->
PrimIO a
- run__IO : IO' l
() ->
PrimIO ()
- replace : (x =
y) ->
P x ->
P y
Perform substitution in a term according to some equality.
This is used by the rewrite tactic and term.
- really_believe_me : a ->
b
Subvert the type checker. This function will reduce in the type checker.
Use it with extreme care - it can result in segfaults or worse!
- prim_write : String ->
IO' l
Int
- prim_read : IO' l
String
- prim_lenString : String ->
Int
- prim_io_return : a ->
PrimIO a
- prim_io_bind : PrimIO a ->
(a ->
PrimIO b) ->
PrimIO b
- prim_fwrite : Ptr ->
String ->
IO' l
Int
- prim_fread : Ptr ->
IO' l
String
- prim_fork : PrimIO () ->
PrimIO Ptr
- prim__zextInt_BigInt : Int ->
Integer
- prim__zextInt_B64 : Int ->
Bits64
- prim__zextInt_B32 : Int ->
Bits32
- prim__zextInt_B16 : Int ->
Bits16
- prim__zextChar_BigInt : Char ->
Integer
- prim__zextB8_Int : Bits8 ->
Int
- prim__zextB8_BigInt : Bits8 ->
Integer
- prim__zextB8_B64 : Bits8 ->
Bits64
- prim__zextB8_B32 : Bits8 ->
Bits32
- prim__zextB8_B16 : Bits8 ->
Bits16
- prim__zextB64_BigInt : Bits64 ->
Integer
- prim__zextB32_Int : Bits32 ->
Int
- prim__zextB32_BigInt : Bits32 ->
Integer
- prim__zextB32_B64 : Bits32 ->
Bits64
- prim__zextB16_Int : Bits16 ->
Int
- prim__zextB16_BigInt : Bits16 ->
Integer
- prim__zextB16_B64 : Bits16 ->
Bits64
- prim__zextB16_B32 : Bits16 ->
Bits32
- prim__xorInt : Int ->
Int ->
Int
- prim__xorChar : Char ->
Char ->
Char
- prim__xorBigInt : Integer ->
Integer ->
Integer
- prim__xorB8 : Bits8 ->
Bits8 ->
Bits8
- prim__xorB64 : Bits64 ->
Bits64 ->
Bits64
- prim__xorB32 : Bits32 ->
Bits32 ->
Bits32
- prim__xorB16 : Bits16 ->
Bits16 ->
Bits16
- prim__writeString : prim__WorldType ->
String ->
Int
- prim__writeFile : prim__WorldType ->
Ptr ->
String ->
Int
- prim__vm : Ptr
- prim__uremInt : Int ->
Int ->
Int
- prim__uremChar : Char ->
Char ->
Char
- prim__uremBigInt : Integer ->
Integer ->
Integer
- prim__uremB8 : Bits8 ->
Bits8 ->
Bits8
- prim__uremB64 : Bits64 ->
Bits64 ->
Bits64
- prim__uremB32 : Bits32 ->
Bits32 ->
Bits32
- prim__uremB16 : Bits16 ->
Bits16 ->
Bits16
- prim__udivInt : Int ->
Int ->
Int
- prim__udivChar : Char ->
Char ->
Char
- prim__udivBigInt : Integer ->
Integer ->
Integer
- prim__udivB8 : Bits8 ->
Bits8 ->
Bits8
- prim__udivB64 : Bits64 ->
Bits64 ->
Bits64
- prim__udivB32 : Bits32 ->
Bits32 ->
Bits32
- prim__udivB16 : Bits16 ->
Bits16 ->
Bits16
- prim__truncInt_B8 : Int ->
Bits8
- prim__truncInt_B64 : Int ->
Bits64
- prim__truncInt_B32 : Int ->
Bits32
- prim__truncInt_B16 : Int ->
Bits16
- prim__truncBigInt_Int : Integer ->
Int
- prim__truncBigInt_Char : Integer ->
Char
- prim__truncBigInt_B8 : Integer ->
Bits8
- prim__truncBigInt_B64 : Integer ->
Bits64
- prim__truncBigInt_B32 : Integer ->
Bits32
- prim__truncBigInt_B16 : Integer ->
Bits16
- prim__truncB64_Int : Bits64 ->
Int
- prim__truncB64_B8 : Bits64 ->
Bits8
- prim__truncB64_B32 : Bits64 ->
Bits32
- prim__truncB64_B16 : Bits64 ->
Bits16
- prim__truncB32_Int : Bits32 ->
Int
- prim__truncB32_B8 : Bits32 ->
Bits8
- prim__truncB32_B16 : Bits32 ->
Bits16
- prim__truncB16_Int : Bits16 ->
Int
- prim__truncB16_B8 : Bits16 ->
Bits8
- prim__toStrInt : Int ->
String
- prim__toStrChar : Char ->
String
- prim__toStrBigInt : Integer ->
String
- prim__toStrB8 : Bits8 ->
String
- prim__toStrB64 : Bits64 ->
String
- prim__toStrB32 : Bits32 ->
String
- prim__toStrB16 : Bits16 ->
String
- prim__toFloatInt : Int ->
Double
- prim__toFloatChar : Char ->
Double
- prim__toFloatBigInt : Integer ->
Double
- prim__toFloatB8 : Bits8 ->
Double
- prim__toFloatB64 : Bits64 ->
Double
- prim__toFloatB32 : Bits32 ->
Double
- prim__toFloatB16 : Bits16 ->
Double
- prim__systemInfo : Int ->
String
- prim__syntactic_eq : (a : Type) ->
(b : Type) ->
(x : a) ->
(y : b) ->
Maybe (x =
y)
- prim__subInt : Int ->
Int ->
Int
- prim__subFloat : Double ->
Double ->
Double
- prim__subChar : Char ->
Char ->
Char
- prim__subBigInt : Integer ->
Integer ->
Integer
- prim__subB8 : Bits8 ->
Bits8 ->
Bits8
- prim__subB64 : Bits64 ->
Bits64 ->
Bits64
- prim__subB32 : Bits32 ->
Bits32 ->
Bits32
- prim__subB16 : Bits16 ->
Bits16 ->
Bits16
- prim__strToFloat : String ->
Double
- prim__strTail : String ->
String
- prim__strRev : String ->
String
- prim__strIndex : String ->
Int ->
Char
- prim__strHead : String ->
Char
- prim__strCons : Char ->
String ->
String
- prim__stdout : Ptr
- prim__stdin : Ptr
- prim__stderr : Ptr
- prim__sremInt : Int ->
Int ->
Int
- prim__sremChar : Char ->
Char ->
Char
- prim__sremBigInt : Integer ->
Integer ->
Integer
- prim__sremB8 : Bits8 ->
Bits8 ->
Bits8
- prim__sremB64 : Bits64 ->
Bits64 ->
Bits64
- prim__sremB32 : Bits32 ->
Bits32 ->
Bits32
- prim__sremB16 : Bits16 ->
Bits16 ->
Bits16
- prim__slteInt : Int ->
Int ->
Int
- prim__slteFloat : Double ->
Double ->
Int
- prim__slteChar : Char ->
Char ->
Int
- prim__slteBigInt : Integer ->
Integer ->
Int
- prim__slteB8 : Bits8 ->
Bits8 ->
Int
- prim__slteB64 : Bits64 ->
Bits64 ->
Int
- prim__slteB32 : Bits32 ->
Bits32 ->
Int
- prim__slteB16 : Bits16 ->
Bits16 ->
Int
- prim__sltInt : Int ->
Int ->
Int
- prim__sltFloat : Double ->
Double ->
Int
- prim__sltChar : Char ->
Char ->
Int
- prim__sltBigInt : Integer ->
Integer ->
Int
- prim__sltB8 : Bits8 ->
Bits8 ->
Int
- prim__sltB64 : Bits64 ->
Bits64 ->
Int
- prim__sltB32 : Bits32 ->
Bits32 ->
Int
- prim__sltB16 : Bits16 ->
Bits16 ->
Int
- prim__shlInt : Int ->
Int ->
Int
- prim__shlChar : Char ->
Char ->
Char
- prim__shlBigInt : Integer ->
Integer ->
Integer
- prim__shlB8 : Bits8 ->
Bits8 ->
Bits8
- prim__shlB64 : Bits64 ->
Bits64 ->
Bits64
- prim__shlB32 : Bits32 ->
Bits32 ->
Bits32
- prim__shlB16 : Bits16 ->
Bits16 ->
Bits16
- prim__sgteInt : Int ->
Int ->
Int
- prim__sgteFloat : Double ->
Double ->
Int
- prim__sgteChar : Char ->
Char ->
Int
- prim__sgteBigInt : Integer ->
Integer ->
Int
- prim__sgteB8 : Bits8 ->
Bits8 ->
Int
- prim__sgteB64 : Bits64 ->
Bits64 ->
Int
- prim__sgteB32 : Bits32 ->
Bits32 ->
Int
- prim__sgteB16 : Bits16 ->
Bits16 ->
Int
- prim__sgtInt : Int ->
Int ->
Int
- prim__sgtFloat : Double ->
Double ->
Int
- prim__sgtChar : Char ->
Char ->
Int
- prim__sgtBigInt : Integer ->
Integer ->
Int
- prim__sgtB8 : Bits8 ->
Bits8 ->
Int
- prim__sgtB64 : Bits64 ->
Bits64 ->
Int
- prim__sgtB32 : Bits32 ->
Bits32 ->
Int
- prim__sgtB16 : Bits16 ->
Bits16 ->
Int
- prim__sextInt_BigInt : Int ->
Integer
- prim__sextInt_B64 : Int ->
Bits64
- prim__sextInt_B32 : Int ->
Bits32
- prim__sextInt_B16 : Int ->
Bits16
- prim__sextChar_BigInt : Char ->
Integer
- prim__sextB8_Int : Bits8 ->
Int
- prim__sextB8_BigInt : Bits8 ->
Integer
- prim__sextB8_B64 : Bits8 ->
Bits64
- prim__sextB8_B32 : Bits8 ->
Bits32
- prim__sextB8_B16 : Bits8 ->
Bits16
- prim__sextB64_BigInt : Bits64 ->
Integer
- prim__sextB32_Int : Bits32 ->
Int
- prim__sextB32_BigInt : Bits32 ->
Integer
- prim__sextB32_B64 : Bits32 ->
Bits64
- prim__sextB16_Int : Bits16 ->
Int
- prim__sextB16_BigInt : Bits16 ->
Integer
- prim__sextB16_B64 : Bits16 ->
Bits64
- prim__sextB16_B32 : Bits16 ->
Bits32
- prim__sdivInt : Int ->
Int ->
Int
- prim__sdivChar : Char ->
Char ->
Char
- prim__sdivBigInt : Integer ->
Integer ->
Integer
- prim__sdivB8 : Bits8 ->
Bits8 ->
Bits8
- prim__sdivB64 : Bits64 ->
Bits64 ->
Bits64
- prim__sdivB32 : Bits32 ->
Bits32 ->
Bits32
- prim__sdivB16 : Bits16 ->
Bits16 ->
Bits16
- prim__registerPtr : Ptr ->
Int ->
ManagedPtr
- prim__readString : prim__WorldType ->
String
- prim__readFile : prim__WorldType ->
Ptr ->
String
- prim__orInt : Int ->
Int ->
Int
- prim__orChar : Char ->
Char ->
Char
- prim__orBigInt : Integer ->
Integer ->
Integer
- prim__orB8 : Bits8 ->
Bits8 ->
Bits8
- prim__orB64 : Bits64 ->
Bits64 ->
Bits64
- prim__orB32 : Bits32 ->
Bits32 ->
Bits32
- prim__orB16 : Bits16 ->
Bits16 ->
Bits16
- prim__null : Ptr
- prim__negFloat : Double ->
Double
- prim__mulInt : Int ->
Int ->
Int
- prim__mulFloat : Double ->
Double ->
Double
- prim__mulChar : Char ->
Char ->
Char
- prim__mulBigInt : Integer ->
Integer ->
Integer
- prim__mulB8 : Bits8 ->
Bits8 ->
Bits8
- prim__mulB64 : Bits64 ->
Bits64 ->
Bits64
- prim__mulB32 : Bits32 ->
Bits32 ->
Bits32
- prim__mulB16 : Bits16 ->
Bits16 ->
Bits16
- prim__lteChar : Char ->
Char ->
Int
- prim__lteBigInt : Integer ->
Integer ->
Int
- prim__lteB8 : Bits8 ->
Bits8 ->
Int
- prim__lteB64 : Bits64 ->
Bits64 ->
Int
- prim__lteB32 : Bits32 ->
Bits32 ->
Int
- prim__lteB16 : Bits16 ->
Bits16 ->
Int
- prim__ltString : String ->
String ->
Int
- prim__ltChar : Char ->
Char ->
Int
- prim__ltBigInt : Integer ->
Integer ->
Int
- prim__ltB8 : Bits8 ->
Bits8 ->
Int
- prim__ltB64 : Bits64 ->
Bits64 ->
Int
- prim__ltB32 : Bits32 ->
Bits32 ->
Int
- prim__ltB16 : Bits16 ->
Bits16 ->
Int
- prim__lshrInt : Int ->
Int ->
Int
- prim__lshrChar : Char ->
Char ->
Char
- prim__lshrBigInt : Integer ->
Integer ->
Integer
- prim__lshrB8 : Bits8 ->
Bits8 ->
Bits8
- prim__lshrB64 : Bits64 ->
Bits64 ->
Bits64
- prim__lshrB32 : Bits32 ->
Bits32 ->
Bits32
- prim__lshrB16 : Bits16 ->
Bits16 ->
Bits16
- prim__intToChar : Int ->
Char
- prim__gteChar : Char ->
Char ->
Int
- prim__gteBigInt : Integer ->
Integer ->
Int
- prim__gteB8 : Bits8 ->
Bits8 ->
Int
- prim__gteB64 : Bits64 ->
Bits64 ->
Int
- prim__gteB32 : Bits32 ->
Bits32 ->
Int
- prim__gteB16 : Bits16 ->
Bits16 ->
Int
- prim__gtChar : Char ->
Char ->
Int
- prim__gtBigInt : Integer ->
Integer ->
Int
- prim__gtB8 : Bits8 ->
Bits8 ->
Int
- prim__gtB64 : Bits64 ->
Bits64 ->
Int
- prim__gtB32 : Bits32 ->
Bits32 ->
Int
- prim__gtB16 : Bits16 ->
Bits16 ->
Int
- prim__fromStrInt : String ->
Int
- prim__fromStrChar : String ->
Char
- prim__fromStrBigInt : String ->
Integer
- prim__fromStrB8 : String ->
Bits8
- prim__fromStrB64 : String ->
Bits64
- prim__fromStrB32 : String ->
Bits32
- prim__fromStrB16 : String ->
Bits16
- prim__fromFloatInt : Double ->
Int
- prim__fromFloatChar : Double ->
Char
- prim__fromFloatBigInt : Double ->
Integer
- prim__fromFloatB8 : Double ->
Bits8
- prim__fromFloatB64 : Double ->
Bits64
- prim__fromFloatB32 : Double ->
Bits32
- prim__fromFloatB16 : Double ->
Bits16
- prim__floatToStr : Double ->
String
- prim__floatTan : Double ->
Double
- prim__floatSqrt : Double ->
Double
- prim__floatSin : Double ->
Double
- prim__floatLog : Double ->
Double
- prim__floatFloor : Double ->
Double
- prim__floatExp : Double ->
Double
- prim__floatCos : Double ->
Double
- prim__floatCeil : Double ->
Double
- prim__floatATan : Double ->
Double
- prim__floatASin : Double ->
Double
- prim__floatACos : Double ->
Double
- prim__eqString : String ->
String ->
Int
- prim__eqInt : Int ->
Int ->
Int
- prim__eqFloat : Double ->
Double ->
Int
- prim__eqChar : Char ->
Char ->
Int
- prim__eqBigInt : Integer ->
Integer ->
Int
- prim__eqB8 : Bits8 ->
Bits8 ->
Int
- prim__eqB64 : Bits64 ->
Bits64 ->
Int
- prim__eqB32 : Bits32 ->
Bits32 ->
Int
- prim__eqB16 : Bits16 ->
Bits16 ->
Int
- prim__divFloat : Double ->
Double ->
Double
- prim__concat : String ->
String ->
String
- prim__complInt : Int ->
Int
- prim__complChar : Char ->
Char
- prim__complBigInt : Integer ->
Integer
- prim__complB8 : Bits8 ->
Bits8
- prim__complB64 : Bits64 ->
Bits64
- prim__complB32 : Bits32 ->
Bits32
- prim__complB16 : Bits16 ->
Bits16
- prim__charToInt : Char ->
Int
- prim__believe_me : (a : Type) ->
(b : Type) ->
(x : a) ->
b
- prim__ashrInt : Int ->
Int ->
Int
- prim__ashrChar : Char ->
Char ->
Char
- prim__ashrBigInt : Integer ->
Integer ->
Integer
- prim__ashrB8 : Bits8 ->
Bits8 ->
Bits8
- prim__ashrB64 : Bits64 ->
Bits64 ->
Bits64
- prim__ashrB32 : Bits32 ->
Bits32 ->
Bits32
- prim__ashrB16 : Bits16 ->
Bits16 ->
Bits16
- prim__andInt : Int ->
Int ->
Int
- prim__andChar : Char ->
Char ->
Char
- prim__andBigInt : Integer ->
Integer ->
Integer
- prim__andB8 : Bits8 ->
Bits8 ->
Bits8
- prim__andB64 : Bits64 ->
Bits64 ->
Bits64
- prim__andB32 : Bits32 ->
Bits32 ->
Bits32
- prim__andB16 : Bits16 ->
Bits16 ->
Bits16
- prim__addInt : Int ->
Int ->
Int
- prim__addFloat : Double ->
Double ->
Double
- prim__addChar : Char ->
Char ->
Char
- prim__addBigInt : Integer ->
Integer ->
Integer
- prim__addB8 : Bits8 ->
Bits8 ->
Bits8
- prim__addB64 : Bits64 ->
Bits64 ->
Bits64
- prim__addB32 : Bits32 ->
Bits32 ->
Bits32
- prim__addB16 : Bits16 ->
Bits16 ->
Bits16
- par : Lazy a ->
a
- mkForeignPrim : ForeignPrimType xs
env
t
- liftPrimIO : (World ->
PrimIO a) ->
IO' l
a
- io_return : a ->
IO' l
a
- io_bind : IO' l
a ->
(a ->
IO' l
b) ->
IO' l
b
- foreign_prim : (f : FFI) ->
(fname : ffi_fn f) ->
FTy f
xs
ty ->
FEnv f
xs ->
ty
- foreign : (f : FFI) ->
(fname : ffi_fn f) ->
(ty : Type) ->
{auto fty : FTy f
[]
ty} ->
ty
- call__IO : IO' l
a ->
PrimIO a
- believe_me : a ->
b
Subvert the type checker. This function is abstract, so it will not reduce in
the type checker. Use it with care - it can result in segfaults or worse!
- assert_total : a ->
a
Assert to the totality checker that the given expression will always
terminate.
- assert_smaller : (x : a) ->
(y : b) ->
b
Assert to the totality checker that y is always structurally smaller than
x (which is typically a pattern argument)
- x
the larger value (typically a pattern argument)
- y
the smaller value (typically an argument to a recursive call)
- applyEnv : (env : FEnv ffi
xs) ->
ForeignPrimType xs
env
t ->
World ->
ffi_fn ffi ->
ffi_types ffi
t ->
PrimIO t
- WorldRes : Type ->
Type
- data World : Type
A token representing the world, for use in IO
- TheWorld : prim__WorldType ->
World
- data Void : Type
The empty type, also known as the trivially false proposition.
Use void or absurd to prove anything if you have a variable of type Void in scope.
- data Unit : Type
The canonical single-element type, also known as the trivially
true proposition.
- MkUnit : ()
The trivial constructor for ().
- data Symbol_ : String ->
Type
For 'symbol syntax. 'foo becomes Symbol_ "foo"
- Ptr : Type
- data PrimIO : Type ->
Type
Idris's primitive IO, for building abstractions on top of
- prim__IO : a ->
PrimIO a
- PE_return_3228af16 : a ->
IO' ffi
a
- PE_map_b7a1b69c : (m : a ->
b) ->
Vect n
a ->
Vect n
b
- PE_List a, TT instance of Language.Reflection.Quotable_c7b7686 : Quotable (List String)
TT
- PE_List a, TT instance of Language.Reflection.Quotable_61e53b8c : Quotable (List ErrorReportPart)
TT
- PE_List a, Raw instance of Language.Reflection.Quotable_1f79f810 : Quotable (List String)
Raw
- PE_@@constructor of Prelude.Monad.Monad#Applicative m_a8f1deca : Applicative (IO' ffi)
- PE_>>=_aaa62508 : IO' ffi
a ->
(a ->
IO' ffi
b) ->
IO' ffi
b
- ManagedPtr : Type
- data LazyType : Type
There are two types of laziness: that arising from lazy functions, and that
arising from codata. They differ in their totality condition.
- LazyCodata : LazyType
- LazyEval : LazyType
- data Lazy' : LazyType ->
Type ->
Type
The underlying implementation of Lazy and Inf.
- Delay : (val : a) ->
Lazy' t
a
A delayed computation.
Delay is inserted automatically by the elaborator where necessary.
Note that compiled code gives Delay special semantics.
- t
whether this is laziness from codata or normal lazy evaluation
- a
the type of the eventual value
- val
a computation that will produce a value
- Lazy : Type ->
Type
Lazily evaluated values. This has special evaluation semantics.
- data JsFn : Type ->
Type
- MkJsFn : (x : t) ->
JsFn t
- data JS_Types : Type ->
Type
- JS_Str : JS_Types String
- JS_Float : JS_Types Double
- JS_Ptr : JS_Types Ptr
- JS_Unit : JS_Types ()
- JS_FnT : JS_FnTypes a ->
JS_Types (JsFn a)
- JS_IntT : JS_IntTypes i ->
JS_Types i
- data JS_IntTypes : Type ->
Type
- JS_IntChar : JS_IntTypes Char
- JS_IntNative : JS_IntTypes Int
- JS_IO : Type ->
Type
- data JS_FnTypes : Type ->
Type
- JS_Fn : JS_Types s ->
JS_FnTypes t ->
JS_FnTypes (s ->
t)
- JS_FnIO : JS_Types t ->
JS_FnTypes (IO' l
t)
- JS_FnBase : JS_Types t ->
JS_FnTypes t
- Inf : Type ->
Type
Recursive parameters to codata. Inserted automatically by the elaborator
on a "codata" definition but is necessary by hand if mixing inductive and
coinductive parameters.
- data IO' : (lang : FFI) ->
Type ->
Type
- MkIO : (World ->
PrimIO a) ->
IO' lang
a
- IO : Type ->
Type
- ForeignPrimType : (xs : List Type) ->
FEnv ffi
xs ->
Type ->
Type
- Force : Lazy' t
a ->
a
Compute a value from a delayed computation.
Inserted by the elaborator where necessary.
- Float : Type
- data FTy : FFI ->
List Type ->
Type ->
Type
- FRet : ffi_types f
t ->
FTy f
xs
(IO' f
t)
- FFun : ffi_types f
s ->
FTy f
(s ::
xs)
t ->
FTy f
xs
(s ->
t)
- FFI_JS : FFI
- data FFI : Type
- MkFFI : (ffi_types : Type ->
Type) ->
(ffi_fn : Type) ->
(ffi_data : Type) ->
FFI
- data (=) : (x : A) ->
(y : B) ->
Type
The propositional equality type. A proof that x = y.
To use such a proof, pattern-match on it, and the two equal things will then need to be the same pattern.
Note: Idris's equality type is potentially heterogeneous, which means that it is possible to state equalities between values of potentially different types. However, Idris will attempt the homogeneous case unless it fails to typecheck.
You may need to use (~=~) to explicitly request heterogeneous equality.
- A
the type of the left side of the equality
- B
the type of the right side of the equality
- Refl : x =
x
A proof that x in fact equals x. To construct this, you must have already shown that both sides are in fact equal.
- A
the type at which the equality is proven
- x
the element shown to be equal to itself.